ePMC - wlan sent 6-0

Log
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property sent
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 16526 16526
build-model-states-explored 37469 20943
build-model-states-explored 56794 19325
build-model-states-explored 77664 20870
build-model-states-explored 102042 24378
build-model-states-explored 125498 23456
build-model-states-explored 147188 21690
build-model-states-explored 170896 23708
build-model-states-explored 194454 23558
build-model-states-explored 217109 22654
build-model-states-explored 244361 27252
build-model-states-explored 271581 27220
build-model-states-explored 298700 27119
build-model-states-explored 325955 27255
build-model-states-explored 353395 27440
build-model-states-explored 381027 27632
build-model-states-explored 408456 27429
build-model-states-explored 432290 23834
build-model-states-explored 451893 19603
build-model-states-explored 469830 17937
build-model-states-explored 493309 23479
build-model-states-explored 516997 23688
build-model-states-explored 540780 23783
build-model-states-explored 564532 23752
build-model-states-explored 588258 23726
build-model-states-explored 613581 25323
build-model-states-explored 639656 26075
build-model-states-explored 665786 26130
build-model-states-explored 691927 26141
build-model-states-explored 717951 26024
build-model-states-explored 743478 25526
build-model-states-explored 764065 20588
build-model-states-explored 789876 25811
build-model-states-explored 816640 26764
build-model-states-explored 843380 26740
build-model-states-explored 865606 22226
build-model-states-explored 892356 26750
build-model-states-explored 919078 26722
build-model-states-explored 945191 26113
build-model-states-explored 972241 27050
build-model-states-explored 999280 27039
build-model-states-explored 1026336 27056
build-model-states-explored 1053314 26978
build-model-states-explored 1080358 27044
build-model-states-explored 1107440 27082
build-model-states-explored 1134501 27060
build-model-states-explored 1161326 26826
build-model-states-explored 1187584 26258
build-model-states-explored 1213866 26282
build-model-states-explored 1240617 26751
build-model-states-explored 1267890 27273
build-model-states-explored 1295249 27359
build-model-states-explored 1322916 27667
build-model-states-explored 1350579 27662
build-model-states-explored 1378243 27665
build-model-states-explored 1405932 27689
build-model-states-explored 1433576 27644
build-model-states-explored 1461282 27706
build-model-states-explored 1488962 27680
build-model-states-explored 1516612 27650
build-model-states-explored 1544245 27633
build-model-states-explored 1569851 25606
build-model-states-explored 1595858 26007
build-model-states-explored 1612890 17032
build-model-states-explored 1631257 18367
build-model-states-explored 1648027 16770
build-model-states-explored 1659679 11652
build-model-states-explored 1677330 17650
build-model-states-explored 1695207 17878
build-model-states-explored 1714664 19457
build-model-states-explored 1734338 19674
build-model-states-explored 1760454 26116
build-model-states-explored 1786566 26112
build-model-states-explored 1812492 25926
build-model-states-explored 1838595 26102
build-model-states-explored 1864657 26063
build-model-states-explored 1890719 26062
build-model-states-explored 1916762 26042
build-model-states-explored 1942830 26069
build-model-states-explored 1968904 26074
build-model-states-explored 1994939 26035
build-model-states-explored 2019016 24077
build-model-states-explored 2045101 26085
build-model-states-explored 2071148 26047
build-model-states-explored 2097151 26003
build-model-states-explored 2123191 26039
build-model-states-explored 2149276 26086
build-model-states-explored 2175393 26117
build-model-states-explored 2201481 26088
build-model-states-explored 2227551 26070
build-model-states-explored 2253606 26055
build-model-states-explored 2279666 26060
build-model-states-explored 2305705 26039
build-model-states-explored 2331713 26008
build-model-states-explored 2357042 25329
build-model-states-explored 2382354 25312
build-model-states-explored 2407662 25308
build-model-states-explored 2432955 25293
build-model-states-explored 2458263 25308
build-model-states-explored 2483567 25304
build-model-states-explored 2508717 25150
build-model-states-explored 2533280 24563
build-model-states-explored 2557983 24703
build-model-states-explored 2574918 16935
build-model-states-explored 2591764 16846
build-model-states-explored 2609737 17973
build-model-states-explored 2635570 25833
build-model-states-explored 2661641 26071
build-model-states-explored 2687720 26079
build-model-states-explored 2713691 25971
build-model-states-explored 2739494 25803
build-model-states-explored 2765676 26181
build-model-states-explored 2789656 23980
build-model-states-explored 2815878 26222
build-model-states-explored 2842100 26222
build-model-states-explored 2868383 26282
build-model-states-explored 2894651 26269
build-model-states-explored 2920931 26280
build-model-states-explored 2947217 26286
build-model-states-explored 2973498 26281
build-model-states-explored 2999722 26224
build-model-states-explored 3026025 26303
build-model-states-explored 3052305 26280
build-model-states-explored 3078585 26280
build-model-states-explored 3104846 26261
build-model-states-explored 3131004 26158
build-model-states-explored 3157251 26247
build-model-states-explored 3183458 26207
build-model-states-explored 3209622 26164
build-model-states-explored 3235761 26139
build-model-states-explored 3261959 26197
build-model-states-explored 3288159 26201
build-model-states-explored 3305265 17106
build-model-states-explored 3322674 17409
build-model-states-explored 3348863 26189
build-model-states-explored 3375086 26223
build-model-states-explored 3401334 26248
build-model-states-explored 3426363 25029
build-model-states-explored 3451424 25061
build-model-states-explored 3476473 25049
build-model-states-explored 3501459 24986
build-model-states-explored 3526492 25032
build-model-states-explored 3551545 25054
build-model-states-explored 3576603 25057
build-model-states-explored 3601627 25025
build-model-states-explored 3626649 25022
build-model-states-explored 3651643 24994
build-model-states-explored 3676684 25041
build-model-states-explored 3701737 25053
build-model-states-explored 3726741 25003
build-model-states-explored 3751782 25041
build-model-states-explored 3776849 25068
build-model-states-explored 3801904 25055
build-model-states-explored 3826921 25017
build-model-states-explored 3851944 25023
build-model-states-explored 3876950 25006
build-model-states-explored 3901991 25041
build-model-states-explored 3927029 25038
build-model-states-explored 3952024 24995
build-model-states-explored 3977069 25045
build-model-states-explored 4002123 25054
build-model-states-explored 4027184 25061
build-model-states-explored 4052229 25044
build-model-states-explored 4077284 25056
build-model-states-explored 4102315 25031
build-model-states-explored 4127372 25057
build-model-states-explored 4152386 25014
build-model-states-explored 4177399 25013
build-model-states-explored 4202649 25250
build-model-states-explored 4228134 25485
build-model-states-explored 4253607 25473
build-model-states-explored 4279099 25492
build-model-states-explored 4304578 25479
build-model-states-explored 4330049 25470
build-model-states-explored 4355534 25486
build-model-states-explored 4381012 25478
build-model-states-explored 4406466 25454
build-model-states-explored 4431949 25483
build-model-states-explored 4457416 25467
build-model-states-explored 4482867 25451
build-model-states-explored 4508328 25461
build-model-states-explored 4533778 25450
build-model-states-explored 4559220 25442
build-model-states-explored 4584679 25459
build-model-states-explored 4610142 25462
build-model-states-explored 4635589 25448
build-model-states-explored 4661082 25493
build-model-states-explored 4686207 25125
build-model-states-explored 4711652 25445
build-model-states-explored 4737140 25488
build-model-states-explored 4762634 25494
build-model-states-explored 4788112 25478
build-model-states-explored 4813576 25464
build-model-states-explored 4839045 25469
build-model-states-explored 4864492 25447
build-model-states-explored 4889967 25475
build-model-states-explored 4915434 25466
build-model-states-explored 4940891 25458
build-model-states-explored 4966358 25467
build-model-states-explored 4986674 20315
build-model-done 5007548 200
iterating
iterating-progress-unbounded 17 1.0 1
iterating-progress-unbounded 38 1.0 2
iterating-progress-unbounded 59 2.0 3
iterating-progress-unbounded 80 2.0 4
iterating-progress-unbounded 101 2.0 5
iterating-progress-unbounded 121 2.0 6
iterating-progress-unbounded 142 2.0 7
iterating-progress-unbounded 163 2.0 8
iterating-progress-unbounded 184 2.0 9
iterating-progress-unbounded 205 2.0 10
iterating-progress-unbounded 226 2.0 11
iterating-progress-unbounded 247 2.0 12
iterating-progress-unbounded 267 2.0 13
iterating-progress-unbounded 288 2.0 14
iterating-progress-unbounded 309 2.0 15
iterating-progress-unbounded 330 2.0 16
iterating-progress-unbounded 351 2.0 17
iterating-progress-unbounded 371 2.0 18
iterating-progress-unbounded 392 2.0 19
iterating-progress-unbounded 413 2.0 20
iterating-progress-unbounded 434 2.0 21
iterating-progress-unbounded 454 2.0 22
iterating-progress-unbounded 475 2.0 23
iterating-progress-unbounded 496 2.0 24
iterating-progress-unbounded 517 2.0 25
iterating-progress-unbounded 537 2.0 26
iterating-progress-unbounded 558 2.0 27
iterating-progress-unbounded 579 2.0 28
iterating-progress-unbounded 600 1.0 29
iterating-progress-unbounded 620 1.0 30
iterating-progress-unbounded 641 1.0 31
iterating-progress-unbounded 662 1.0 32
iterating-progress-unbounded 682 1.0 33
iterating-progress-unbounded 703 2.0 34
iterating-progress-unbounded 724 2.0 35
iterating-progress-unbounded 744 1.0 36
iterating-progress-unbounded 765 1.0 37
iterating-progress-unbounded 785 1.0 38
iterating-progress-unbounded 806 1.0 39
iterating-progress-unbounded 827 1.0 40
iterating-progress-unbounded 847 2.0 41
iterating-progress-unbounded 868 2.0 42
iterating-progress-unbounded 888 1.0 43
iterating-progress-unbounded 909 1.0 44
iterating-progress-unbounded 929 1.0 45
iterating-progress-unbounded 950 1.0 46
iterating-progress-unbounded 970 1.0 47
iterating-progress-unbounded 991 2.0 48
iterating-progress-unbounded 1011 1.0 49
iterating-progress-unbounded 1032 1.0 50
iterating-progress-unbounded 1052 1.0 51
iterating-progress-unbounded 1073 1.0 52
iterating-progress-unbounded 1093 1.0 53
iterating-progress-unbounded 1114 1.0 54
iterating-progress-unbounded 1134 2.0 55
iterating-progress-unbounded 1155 1.0 56
iterating-progress-unbounded 1175 1.0 57
iterating-progress-unbounded 1195 1.0 58
iterating-progress-unbounded 1216 1.0 59
iterating-progress-unbounded 1236 1.0 60
iterating-progress-unbounded 1256 1.0 61
iterating-progress-unbounded 1277 1.0 62
iterating-progress-unbounded 1297 1.0 63
iterating-progress-unbounded 1317 1.0 64
iterating-progress-unbounded 1338 1.0 65
iterating-progress-unbounded 1358 2.0 66
iterating-progress-unbounded 1378 1.0 67
iterating-progress-unbounded 1398 1.0 68
iterating-progress-unbounded 1419 1.0 69
iterating-progress-unbounded 1439 1.0 70
iterating-progress-unbounded 1459 1.0 71
iterating-progress-unbounded 1479 1.0 72
iterating-progress-unbounded 1499 1.0 73
iterating-progress-unbounded 1520 1.0 74
iterating-progress-unbounded 1540 1.0 75
iterating-progress-unbounded 1560 1.0 76
iterating-progress-unbounded 1580 1.0 77
iterating-progress-unbounded 1600 1.0 78
iterating-progress-unbounded 1620 1.0 79
iterating-progress-unbounded 1640 1.0 80
iterating-progress-unbounded 1661 1.0 81
iterating-progress-unbounded 1681 1.0 82
iterating-progress-unbounded 1701 1.0 83
iterating-progress-unbounded 1721 1.0 84
iterating-progress-unbounded 1741 1.0 85
iterating-progress-unbounded 1761 1.0 86
iterating-progress-unbounded 1781 1.0 87
iterating-progress-unbounded 1801 1.0 88
iterating-progress-unbounded 1821 1.0 89
iterating-progress-unbounded 1841 1.0 90
iterating-progress-unbounded 1861 1.0 91
iterating-progress-unbounded 1881 1.0 92
iterating-progress-unbounded 1901 1.0 93
iterating-progress-unbounded 1921 1.0 94
iterating-progress-unbounded 1941 1.0 95
iterating-progress-unbounded 1961 1.0 96
iterating-progress-unbounded 1981 1.0 97
iterating-progress-unbounded 2001 1.0 98
iterating-progress-unbounded 2021 1.0 99
iterating-progress-unbounded 2041 1.0 100
iterating-progress-unbounded 2061 1.0 101
iterating-progress-unbounded 2081 1.0 102
iterating-progress-unbounded 2101 1.0 103
iterating-progress-unbounded 2121 1.0 104
iterating-progress-unbounded 2141 0.1 105
iterating-progress-unbounded 2161 0.05000009536739266 106
iterating-progress-unbounded 2181 0.033333587645483935 107
iterating-progress-unbounded 2201 0.025000336400486867 108
iterating-progress-unbounded 2221 0.02000038101849557 109
iterating-progress-unbounded 2241 0.016667074191369386 110
iterating-progress-unbounded 2261 0.014286138737514909 111
iterating-progress-unbounded 2281 0.012500435887716533 112
iterating-progress-unbounded 2301 0.01111155507526129 113
iterating-progress-unbounded 2321 0.010000449874755039 114
iterating-progress-unbounded 2341 0.00909136341910607 115
iterating-progress-unbounded 2361 0.008333791099376183 116
iterating-progress-unbounded 2381 0.007692768167077763 117
iterating-progress-unbounded 2401 0.00714331978955504 118
iterating-progress-unbounded 2421 0.006667131081430076 119
iterating-progress-unbounded 2441 0.006250465873211081 120
iterating-progress-unbounded 2461 0.005882820031521114 121
iterating-progress-unbounded 2481 0.005556023672192784 122
iterating-progress-unbounded 2501 0.0052636268847721275 123
iterating-progress-unbounded 2521 0.005000469739508266 124
iterating-progress-unbounded 2541 0.004762375149384764 125
iterating-progress-unbounded 2561 0.004545925496980395 126
iterating-progress-unbounded 2581 0.004348297532534216 127
iterating-progress-unbounded 2601 0.004167138547459234 128
iterating-progress-unbounded 2621 0.004000472266191642 129
iterating-progress-unbounded 2641 0.0038392901853054567 130
iterating-progress-unbounded 2661 0.003697371890969867 131
iterating-progress-unbounded 2681 0.003565572796247745 132
iterating-progress-unbounded 2701 0.0034428478956679844 133
iterating-progress-unbounded 2721 0.003328291248377287 134
iterating-progress-unbounded 2741 0.003221113625690436 135
iterating-progress-unbounded 2761 0.0031206243024037303 136
iterating-progress-unbounded 2781 0.003026216153942033 137
iterating-progress-unbounded 2801 0.0029373533796924977 138
iterating-progress-unbounded 2821 0.002853561328004283 139
iterating-progress-unbounded 2841 0.002774418014741099 140
iterating-progress-unbounded 2861 0.0026995470154078213 141
iterating-progress-unbounded 2881 0.0026286114781417223 142
iterating-progress-unbounded 2901 0.0025613090566351422 143
iterating-progress-unbounded 2921 0.002497367602197295 144
iterating-progress-unbounded 2941 0.0024365414855006943 145
iterating-progress-unbounded 2961 0.0023786084431846335 146
iterating-progress-unbounded 2981 0.002323366863967847 147
iterating-progress-unbounded 3001 0.002270633444427115 148
iterating-progress-unbounded 3021 0.0022202411570031084 149
iterating-progress-unbounded 3041 0.0021720374827669405 150
iterating-progress-unbounded 3061 0.0021258828695530155 151
iterating-progress-unbounded 3081 0.002081649382637325 152
iterating-progress-unbounded 3101 0.0020392195204656355 153
iterating-progress-unbounded 3121 0.0019984851723613825 154
iterating-progress-unbounded 3141 0.0019593466987368633 155
iterating-progress-unbounded 3161 0.0018527815062308896 156
iterating-progress-unbounded 3181 0.0017515921948949695 157
iterating-progress-unbounded 3201 0.0016584648031024172 158
iterating-progress-unbounded 3221 0.0015724277006683122 159
iterating-progress-unbounded 3241 0.001492658058645748 160
iterating-progress-unbounded 3261 0.0014184542158758614 161
iterating-progress-unbounded 3281 0.001349214111642076 162
iterating-progress-unbounded 3302 0.0012827727239698113 163
iterating-progress-unbounded 3322 0.0012221222744628756 164
iterating-progress-unbounded 3341 0.001166413188421386 165
iterating-progress-unbounded 3361 0.0011124666450001764 166
iterating-progress-unbounded 3382 0.0010603493107628756 167
iterating-progress-unbounded 3402 0.0010121267243794008 168
iterating-progress-unbounded 3422 9.663360821967567E-4 169
iterating-progress-unbounded 3442 9.227751545192776E-4 170
iterating-progress-unbounded 3462 8.812556732310401E-4 171
iterating-progress-unbounded 3482 8.416088066207435E-4 172
iterating-progress-unbounded 3502 8.036826634860625E-4 173
iterating-progress-unbounded 3522 7.673401694012001E-4 174
iterating-progress-unbounded 3542 7.324572517990031E-4 175
iterating-progress-unbounded 3562 6.989212825296471E-4 176
iterating-progress-unbounded 3582 6.666297360781916E-4 177
iterating-progress-unbounded 3603 6.330903696840618E-4 178
iterating-progress-unbounded 3623 6.030856222681191E-4 179
iterating-progress-unbounded 3643 5.740603590318619E-4 180
iterating-progress-unbounded 3663 5.459427150966847E-4 181
iterating-progress-unbounded 3683 5.186664023569408E-4 182
iterating-progress-unbounded 3703 4.921701182028018E-4 183
iterating-progress-unbounded 3723 4.6639702012038774E-4 184
iterating-progress-unbounded 3743 4.412942831482323E-4 185
iterating-progress-unbounded 3763 4.1681268643561903E-4 186
iterating-progress-unbounded 3783 3.9290625076757266E-4 187
iterating-progress-unbounded 3804 3.6918802641615074E-4 188
iterating-progress-unbounded 3824 3.4633827973195956E-4 189
iterating-progress-unbounded 3844 3.239276237507168E-4 190
iterating-progress-unbounded 3864 3.018985748659956E-4 191
iterating-progress-unbounded 3884 2.802558721672439E-4 192
iterating-progress-unbounded 3904 2.589671866555374E-4 193
iterating-progress-unbounded 3924 2.3800174078809422E-4 194
iterating-progress-unbounded 3944 2.1733014679062204E-4 195
iterating-progress-unbounded 3964 1.9692425801695246E-4 196
iterating-progress-unbounded 3984 1.767570317521726E-4 197
iterating-progress-unbounded 4004 1.568024019516678E-4 198
iterating-progress-unbounded 4024 1.370351606074191E-4 199
iterating-progress-unbounded 4044 1.1743084656607934E-4 200
iterating-progress-unbounded 4064 9.796564071128225E-5 201
iterating-progress-unbounded 4084 7.861626655799518E-5 202
iterating-progress-unbounded 4103 6.023704899566629E-5 203
iterating-progress-unbounded 4123 4.1067905200129925E-5 204
iterating-progress-unbounded 4143 2.19433984469096E-5 205
iterating-progress-unbounded 4164 2.383812023344642E-6 206
iterating-progress-unbounded 4184 1.4292232892495184E-6 207
iterating-progress-unbounded 4204 1.429190495132374E-6 208
iterating-progress-unbounded 4224 1.4287259915676086E-6 209
iterating-progress-unbounded 4244 1.427715073434715E-6 210
iterating-progress-unbounded 4264 1.426157775528312E-6 211
iterating-progress-unbounded 4284 1.4240541290577126E-6 212
iterating-progress-unbounded 4304 1.421404166034507E-6 213
iterating-progress-unbounded 4324 1.41820791587779E-6 214
iterating-progress-unbounded 4345 1.4141439989852152E-6 215
iterating-progress-unbounded 4365 1.4098552786230656E-6 216
iterating-progress-unbounded 4385 1.4050203603783858E-6 217
iterating-progress-unbounded 4405 1.3996392741350207E-6 218
iterating-progress-unbounded 4425 1.3937120489965169E-6 219
iterating-progress-unbounded 4445 1.3872387040014006E-6 220
iterating-progress-unbounded 4465 1.3802190637894836E-6 221
iterating-progress-unbounded 4485 1.3726530838760952E-6 222
iterating-progress-unbounded 4505 1.3645408126763944E-6 223
iterating-progress-unbounded 4525 1.3558822941906192E-6 224
iterating-progress-unbounded 4546 1.3460558908853292E-6 225
iterating-progress-unbounded 4566 1.3362532249813046E-6 226
iterating-progress-unbounded 4586 1.325904794651479E-6 227
iterating-progress-unbounded 4606 1.3150106005399835E-6 228
iterating-progress-unbounded 4626 1.3035706393575839E-6 229
iterating-progress-unbounded 4646 1.2915849102672213E-6 230
iterating-progress-unbounded 4666 1.2790534080460593E-6 231
iterating-progress-unbounded 4686 1.2659761278040737E-6 232
iterating-progress-unbounded 4706 1.252353972787121E-6 233
iterating-progress-unbounded 4726 1.2381966232759945E-6 234
iterating-progress-unbounded 4747 1.223083384934379E-6 235
iterating-progress-unbounded 4767 1.2078093566897418E-6 236
iterating-progress-unbounded 4787 1.1919895686866257E-6 237
iterating-progress-unbounded 4807 1.175624048699957E-6 238
iterating-progress-unbounded 4827 1.158712821525429E-6 239
iterating-progress-unbounded 4847 1.1412559104754353E-6 240
iterating-progress-unbounded 4867 1.1232533375417493E-6 241
iterating-progress-unbounded 4887 1.1047051221140836E-6 242
iterating-progress-unbounded 4907 1.0856109097973493E-6 243
iterating-progress-unbounded 4928 1.064587109007181E-6 244
iterating-progress-unbounded 4948 1.0443702620291272E-6 245
iterating-progress-unbounded 4968 1.0236082802568551E-6 246
iterating-progress-unbounded 4988 1.0023011066053866E-6 247
iterating-progress-unbounded 5008 9.804486829223924E-7 248
iterating-progress-unbounded 5028 9.580509457077553E-7 249
iterating-progress-unbounded 5048 9.351078316073705E-7 250
iterating-progress-unbounded 5068 9.116192747986409E-7 251
iterating-progress-unbounded 5088 8.875852050426045E-7 252
iterating-progress-unbounded 5109 8.621278923193411E-7 253
iterating-progress-unbounded 5129 8.369686475575196E-7 254
iterating-progress-unbounded 5149 8.112631349263935E-7 255
iterating-progress-unbounded 5169 7.850113645295403E-7 256
iterating-progress-unbounded 5189 7.582133442984171E-7 257
iterating-progress-unbounded 5209 7.308690777116857E-7 258
iterating-progress-unbounded 5229 7.030942220324031E-7 259
iterating-progress-unbounded 5249 6.757214939511561E-7 260
iterating-progress-unbounded 5269 6.488940998830072E-7 261
iterating-progress-unbounded 5290 6.210168624651093E-7 262
iterating-progress-unbounded 5310 5.953163564040437E-7 263
iterating-progress-unbounded 5330 5.701610602982895E-7 264
iterating-progress-unbounded 5350 5.455509423746859E-7 265
iterating-progress-unbounded 5370 5.214859747947074E-7 266
iterating-done 5390 267
model-checking-done 475
command-check-result-is true sent
Model:	wlan v.1 (MDP)
Parameter(s)	MAX_BACKOFF = 6, COL = 0
Property:	sent (prob-reach)
Walltime:	476.01034450531006s
Return code:	0